sends-p(es; ds; k; T; l; dt; g)
== ((x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top)))
==  (e:es-E(es). 
==  (es-isrcv(es; e))
==   (es-lnk(es; e) = l)
==   subtype_rel(es-valtype(es; e); fpf-cap(dt; id-deq; es-tag(es; e); top))))
== c alle-at(es;
== c alle-at(source(l);
== c alle-at(e.((es-kind(es; e) = k)
== c alle-at( (subtype_rel(es-valtype(es; e); T)
== c alle-at( c (L:{e:es-E(es)| 
== c alle-at( c (L:{(es-isrcv(es; e))
== c alle-at( c (L:{c ((es-lnk(es; e) = l)  (fpf-dom(id-deq; es-tag(es; e); dt)))}  List
== c alle-at( c ((es-rcv-from(es; e; l; L)
== c alle-at( c (c (map((e.<es-tag(es; e), es-val(es; e)>); L)
== c alle-at( c (c (=
== c alle-at( c (c (concat(map((tgf.sends-msgs(es-state-when(es; e); es-val(es; e); tgf)); g)
== c alle-at( c (c (concat())))))) 

latex

---

clarification:

sends-p(es; ds; k; T; l; dt; g)
== ((x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top)))
==  (e:es-E(es). 
==  (es-isrcv(es; e))
==   (es-lnk(es; e) = l  IdLnk)
==   subtype_rel(es-valtype(es; e); fpf-cap(dt; id-deq; es-tag(es; e); top))))
== c alle-at(es;
== c alle-at(source(l);
== c alle-at(e.((es-kind(es; e) = k  Knd)
== c alle-at( (subtype_rel(es-valtype(es; e); T)
== c alle-at( c (L:{e:es-E(es)| 
== c alle-at( c (L:{(es-isrcv(es; e))
== c alle-at( c (L:{c ((es-lnk(es; e) = l  IdLnk)
== c alle-at( c (L:{c  (fpf-dom(id-deq; es-tag(es; e); dt)))}  List
== c alle-at( c ((es-rcv-from(es; e; l; L)
== c alle-at( c (c (map((e.<es-tag(es; e), es-val(es; e)>); L)
== c alle-at( c (c (=
== c alle-at( c (c (concat(map((tgf.sends-msgs(es-state-when(es; e); es-val(es; e); tgf)); g)
== c alle-at( c (c (concat()
== c alle-at( c (c ( ((tg:Id  fpf-cap(dt; id-deq; tg; void)) List))))))) 

latex

Definitions

sends-p(es; ds; k; T; l; dt; g), es-vartype(es; i; x), x:A. B(x), top, alle-at(es; i; e.P(e)), source(l), P  Q, Knd, es-kind(es; e), es-valtype(es; e), x:A. B(x), es-E(es), es-isrcv(es; e), P  Q, IdLnk, es-lnk(es; e), b, fpf-dom(eq; x; f), A c B, es-rcv-from(es; e; l; L), Id, fpf-cap(f; eq; x; z), id-deq, es-tag(es; e), concat(ll), map(f; as), sends-msgs(s; v; tg_f), es-state-when(es; e), es-val(es; e)

FDL editor aliases

sends-p